{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 逻辑\n",
    "\n",
    "原文: https://docs.sympy.org/latest/modules/logic.html\n",
    "\n",
    "SymPy 的逻辑模块允许使用符号和布尔值形成和操作逻辑表达式。\n",
    "\n",
    "## Forming logical expressions 形成逻辑表达式\n",
    "\n",
    "可以使用标准的 python 运算符 `&` (And)、 `|` (Or)、 `~` (Not)来构建布尔表达式:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 131,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "y | (x & y)\n",
      "x | y\n",
      "~x\n"
     ]
    }
   ],
   "source": [
    "from sympy import *\n",
    "x, y = symbols('x,y')\n",
    "print(y | (x & y))\n",
    "print(x | y)\n",
    "print(~x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "也可以使用 `>>` 和 `<<` :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 132,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Implies(x, y)\n",
      "Implies(y, x)\n"
     ]
    }
   ],
   "source": [
    "print(x >> y)\n",
    "print(x << y)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "与 SymPy 中的大多数类型一样，布尔表达式继承自 Basic:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 133,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "{y, x}\n"
     ]
    }
   ],
   "source": [
    "print((y & x).subs({x: True, y: True}))\n",
    "print((x | y).atoms())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "逻辑模块还包括以下函数，用于从真值表中推导布尔表达式:\n",
    "\n",
    "### 方法 sympy.logic.boolalg.SOPform(variables, minterms, dontcares=None)\n",
    "\n",
    "The SOPform function uses simplified_pairs and a redundant group- eliminating algorithm to convert the list of all input combos that generate ‘1’ (the minterms) into the smallest Sum of Products form.\n",
    "\n",
    "SOPform 函数使用 `simplified_pairs` 和冗余的 `group-eliminating` 消组算法将生成“1”(最小项)的所有输入的由`1`组合成的真值列表转换为最小合取形式。\n",
    "\n",
    "`variables`必须作为第一个参数。\n",
    "\n",
    "返回一个逻辑的或函数(例如， `sum of products` 或 `SOP` 形式) ，给出期望的结果。如果有可以忽略的输入，也将它们作为列表传递。\n",
    "\n",
    "结果将是满足条件的函数(可能有很多)之一。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 134,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(y \\wedge z\\right) \\vee \\left(\\neg w \\wedge \\neg x\\right)$"
      ],
      "text/plain": [
       "(y & z) | (~w & ~x)"
      ]
     },
     "execution_count": 134,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.logic import SOPform\n",
    "from sympy import symbols\n",
    "w, x, y, z = symbols('w x y z')\n",
    "minterms = [[0, 0, 0, 1], [0, 0, 1, 1],\n",
    "            [0, 1, 1, 1], [1, 0, 1, 1], [1, 1, 1, 1]]\n",
    "dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]\n",
    "SOPform([w, x, y, z], minterms, dontcares)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "这些`term`因式真值表也可以表示为整数:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 135,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(y \\wedge z\\right) \\vee \\left(\\neg w \\wedge \\neg x\\right)$"
      ],
      "text/plain": [
       "(y & z) | (~w & ~x)"
      ]
     },
     "execution_count": 135,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minterms = [1, 3, 7, 11, 15]\n",
    "dontcares = [0, 2, 5]\n",
    "SOPform([w, x, y, z], minterms, dontcares)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "也可以使用字典来指定，但不必完全指定:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 136,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(x \\wedge \\neg w\\right) \\vee \\left(y \\wedge z \\wedge \\neg x\\right)$"
      ],
      "text/plain": [
       "(x & ~w) | (y & z & ~x)"
      ]
     },
     "execution_count": 136,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}]\n",
    "SOPform([w, x, y, z], minterms)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "或者一个组合:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 137,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(\\neg w \\wedge \\neg y\\right) \\vee \\left(w \\wedge y \\wedge z\\right) \\vee \\left(x \\wedge z \\wedge \\neg w\\right)$"
      ],
      "text/plain": [
       "(w & y & z) | (~w & ~y) | (x & z & ~w)"
      ]
     },
     "execution_count": 137,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minterms = [4, 7, 11, [1, 1, 1, 1]]\n",
    "dontcares = [{w : 0, x : 0, y: 0}, 5]\n",
    "SOPform([w, x, y, z], minterms, dontcares)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 参考资料\n",
    "\n",
    "[R552] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm\n",
    "\n",
    "### 方法 sympy.logic.boolalg.POSform(variables, minterms, dontcares=None)\n",
    "\n",
    "POSform 函数使用 `simplified_pairs` 和冗余`redundant-group`组消除算法将所有输入“1”(最小项)的组合的真值表, 转换为最小析取式。\n",
    "\n",
    "`variables`必须作为第一个参数。\n",
    "\n",
    "返回一个逻辑和函数(即`product of sums`或`POS`形式) ，它给出所需的结果。如果有可以忽略的输入，也将它们作为列表传递。\n",
    "\n",
    "结果将是满足条件的函数(可能有很多)之一。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 138,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle z \\wedge \\left(y \\vee \\neg w\\right)$"
      ],
      "text/plain": [
       "z & (y | ~w)"
      ]
     },
     "execution_count": 138,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.logic import POSform\n",
    "from sympy import symbols\n",
    "w, x, y, z = symbols('w x y z')\n",
    "minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1],\n",
    "            [1, 0, 1, 1], [1, 1, 1, 1]]\n",
    "dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]\n",
    "POSform([w, x, y, z], minterms, dontcares)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "这些术语也可以表示为整数:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 139,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle z \\wedge \\left(y \\vee \\neg w\\right)$"
      ],
      "text/plain": [
       "z & (y | ~w)"
      ]
     },
     "execution_count": 139,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minterms = [1, 3, 7, 11, 15]\n",
    "dontcares = [0, 2, 5]\n",
    "POSform([w, x, y, z], minterms, dontcares)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "也可以使用字典来指定，但不必完全指定:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 140,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(x \\vee y\\right) \\wedge \\left(x \\vee z\\right) \\wedge \\left(\\neg w \\vee \\neg x\\right)$"
      ],
      "text/plain": [
       "(x | y) & (x | z) & (~w | ~x)"
      ]
     },
     "execution_count": 140,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}]\n",
    "POSform([w, x, y, z], minterms)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "或者一个组合:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 141,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(w \\vee x\\right) \\wedge \\left(y \\vee \\neg w\\right) \\wedge \\left(z \\vee \\neg y\\right)$"
      ],
      "text/plain": [
       "(w | x) & (y | ~w) & (z | ~y)"
      ]
     },
     "execution_count": 141,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "minterms = [4, 7, 11, [1, 1, 1, 1]]\n",
    "dontcares = [{w : 0, x : 0, y: 0}, 5]\n",
    "POSform([w, x, y, z], minterms, dontcares)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 参考资料\n",
    "\n",
    "[R553] https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm\n",
    "\n",
    "### 函数 sympy.logic.boolalg.ANFform(variables, truthvalues)\n",
    "\n",
    "函数将真值列表转换为代数范式(ANF)。\n",
    "\n",
    "`variables`必须作为第一个参数。\n",
    "\n",
    "返回 `True`，`False`，`logical` 和 `funciton` (即`Zhegalkin monomial`哲加尔金单项式)或者逻辑 `Xor` 函数(即`Zhegalkin monomial`哲加尔金多项式)。当 `True` 和 `False` 分别用`1`和`0`表示时，`And` 表示乘法，`Xor` 表示加法。\n",
    "\n",
    "形式上，`Zhegalkin 单项式`是有限个离散变量集的乘积(逻辑和) ，包括乘积为1(真)的空集。一个`Zhegalkin 多项式`是 `Zhegalkin 单项式`集合的和(逻辑 Xor) ，其空集由`0`(`False`)表示。\n",
    "\n",
    "#### 参数 variables : 变量列表\n",
    "\n",
    "真值: `1`和`0`的列表(真值表的结果列)\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 142,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x ^ True\n",
      "x ^ y ^ (x & y)\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import ANFform\n",
    "from sympy.abc import x, y\n",
    "print(ANFform([x], [1, 0]))\n",
    "print(ANFform([x, y], [0, 1, 1, 1]))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 参考资料\n",
    "\n",
    "[R554] https://en.wikipedia.org/wiki/Zhegalkin_polynomial\n",
    "\n",
    "## Boolean functions 布尔函数\n",
    "\n",
    "### class 类 sympy.logic.boolalg.Boolean(*args)\n",
    "\n",
    "布尔对象是逻辑操作有意义的对象。\n",
    "\n",
    "#### as_set()\n",
    "\n",
    "按实数集重写布尔表达式。\n",
    "\n",
    "##### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 143,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "FiniteSet(0)\n",
      "Interval.open(0, oo)\n",
      "Interval.open(-2, 2)\n",
      "Union(Interval.open(-oo, -2), Interval.open(2, oo))\n"
     ]
    }
   ],
   "source": [
    "from sympy import Symbol, Eq, Or, And\n",
    "x = Symbol('x', real=True)\n",
    "print(Eq(x, 0).as_set())\n",
    "print((x > 0).as_set())\n",
    "print(And(-2 < x, x < 2).as_set())\n",
    "print(Or(x < -2, 2 < x).as_set())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### equals(other)\n",
    "\n",
    "如果给定的公式具有相同的真值表，则返回 `True`。要使两个公式相等，它们必须具有相同的文字量。\n",
    "\n",
    "##### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 144,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy.abc import A, B, C\n",
    "from sympy import And, Or, Not\n",
    "print((A >> B).equals(~B >> ~A))\n",
    "print(Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C))))\n",
    "print(Not(And(A, Not(A))).equals(Or(B, Not(B))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.BooleanTrue\n",
    "\n",
    "`True` 的 SymPy 版本，一个可以通过 `s.True` 访问的单例模式。\n",
    "\n",
    "这是 `True` 的 `SymPy` 版本，用于逻辑模块。使用 `true` 而不是 `True` 的主要优点是，像 `~` 和 `>>` 这样的简写布尔操作在这个类上可以正常工作，而在 `True` 中，它们在`1`上按位运行。逻辑模块中的函数在计算为 `true` 时将返回此类。\n",
    "\n",
    "#### 注释\n",
    "\n",
    "在什么时候应该使用 `True` 和什么时候应该使用 `S.True` 这两个问题上可能会有些混淆。需要记住的一件重要事情是 `sympify(True)`返回 `s.True`。这意味着在大多数情况下，只需要使用 `True`，它就会在必要时自动转换为 `s.True`，就像你通常使用`1`代替 `S.One` 一样。\n",
    "\n",
    "经验法则是:\n",
    "\n",
    "如果所讨论的布尔值可以被任意符号布尔值代替，比如 `Or(x，y)`或者 `x > 1`，使用 `S.true`, 否则，使用 `True`\n",
    "\n",
    "换句话说，只有在布尔值被用作真值的符号表示的上下文中才使用 `S.true`。例如，如果对象最终位于任何表达式中`.args`的元素，那么它必须是 `S.True` 而不是 `True`。`.arg`的元素必须是`Basic`的。另一方面，`==` 在 SymPy 中不是一个符号操作，因为它总是返回 `True` 或 `False`，并且这样做是基于结构相等而不是数学，所以它应该返回 `True`。假设`assumptions`系统应该使用 `True` 和 `False`。除了不能满足上述的经验法则外，这个假设系统使用一个三值逻辑(`True`，`False`，`None`) ，而 `s.True` 和 `s.False` 代表一个两值逻辑。如果有疑问，使用 `True`。\n",
    "\n",
    "`S.true == True is True`\n",
    "\n",
    "`S.true is True` 为 `False`, `S.true == True`为 `True`, 如果对函数或表达式返回`S.true`或者`True`有任何疑问，只需使用 `==` 来代替 `is` 进行比较，两种情况都可以。最后，对于布尔标志，最好只使用 `if x` 而不是 `if x is True`。引用 PEP 8:\n",
    "\n",
    "不要用 `==` 比较布尔值与 `True` 或 `False。`\n",
    "\n",
    "- Yes: if greeting:\n",
    "- No: if greeting == True:\n",
    "- Worse: if greeting is True:\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 145,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False False\n",
      "True\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 145,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import sympify, true, false, Or\n",
    "print(sympify(True))\n",
    "print(_ is True, _ is true)\n",
    "print(Or(true, false))\n",
    "(_ is true)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Python 运算符为 True 提供一个布尔结果，但为 True 提供一个按位结果"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 146,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False -2\n",
      "True 0\n"
     ]
    }
   ],
   "source": [
    "print(~true, ~True)\n",
    "print(true >> true, True >> True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "> See also参见 sympy.logic.boolalg.BooleanFalse\n",
    "\n",
    "### as_set()\n",
    "\n",
    "根据实集重写逻辑运算符和关系。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 147,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\mathbb{U}$"
      ],
      "text/plain": [
       "UniversalSet"
      ]
     },
     "execution_count": 147,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import true\n",
    "true.as_set()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.BooleanFalse\n",
    "\n",
    "`False`的 `SymPy` 版本，这是一个可以通过 `s.false` 访问的单例模式。\n",
    "\n",
    "This is the SymPy version of False, for use in the logic module. The primary advantage of using false instead of False is that shorthand Boolean operations like ~ and >> will work as expected on this class, whereas with False they act bitwise on 0. Functions in the logic module will return this class when they evaluate to false.\n",
    "\n",
    "这是 `False` 的 `SymPy` 版本，用于逻辑模块。使用 `false` 而不是 `False` 的主要优点是，像 `~` 和 `>>` 这样的简写布尔操作在这个类上可以正常工作，而使用 `False` 时，它们在`0`上按位运行。逻辑模块中的函数在计算为 `false` 时将返回此类。\n",
    "\n",
    "#### 注释\n",
    "\n",
    "请参阅 sympy.logic.boolalg.BooleanTrue 中的注释部分\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 148,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "False False\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy import sympify, true, false, Or\n",
    "print(sympify(False))\n",
    "print(_ is False, _ is false)\n",
    "print(Or(true, false))\n",
    "print(_ is true)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Python 运算符给出 `false` 的布尔结果，而给出 `False` 的按位结果"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 149,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True -1\n",
      "True 0\n"
     ]
    }
   ],
   "source": [
    "print(~false, ~False)\n",
    "print(false >> false, False >> False)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "> 参见 sympy.logic.boolalg.BooleanTrue\n",
    "\n",
    "#### as_set 准备就绪()\n",
    "\n",
    "根据实集重写逻辑运算符和关系。\n",
    "\n",
    "##### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 150,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\emptyset$"
      ],
      "text/plain": [
       "EmptySet"
      ]
     },
     "execution_count": 150,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import false\n",
    "false.as_set()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.And(*args)\n",
    "\n",
    "逻辑与(`AND`)函数。\n",
    "\n",
    "它按顺序计算自己的参数，当参数为 `false` 时立即返回 `false`，当所有参数为 `true` 时立即返回 `true`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 151,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle x \\wedge y$"
      ],
      "text/plain": [
       "x & y"
      ]
     },
     "execution_count": 151,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.abc import x, y\n",
    "from sympy import And\n",
    "x & y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 注释\n",
    "\n",
    "提供 `&` 操作符是为了方便，但请注意，这里使用的 `&` 操作符与 Python 中的正常使用不同，Python 中的正常使用是按位和。因此，如果 `a`, `b` 是整数，`AND(a，b)`和 `a & b` 将返回不同的结果。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 152,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle y$"
      ],
      "text/plain": [
       "y"
      ]
     },
     "execution_count": 152,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "And(x, y).subs(x, 1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Or(*args)\n",
    "\n",
    "逻辑或(`OR`)函数\n",
    "\n",
    "它按顺序计算自己的参数，当参数为真时立即返回 `true`，当参数全部为假时返回 `false`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 153,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle x \\vee y$"
      ],
      "text/plain": [
       "x | y"
      ]
     },
     "execution_count": 153,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.abc import x, y\n",
    "from sympy import Or\n",
    "x | y"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 注释\n",
    "\n",
    "提供 `|` 操作符是为了方便，但请注意，它在这里的使用与 Python 中的正常使用不同，Python 中的正常使用是按位或。因此，如果 `a` 和 `b` 是整数，`Or (a，b)`和 `a | b` 将返回不同的结果。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 154,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle y$"
      ],
      "text/plain": [
       "y"
      ]
     },
     "execution_count": 154,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Or(x, y).subs(x, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Not(arg)\n",
    "\n",
    "逻辑非(`NOT`)函数(否定)\n",
    "\n",
    "Returns true if the statement is false or False. Returns false if the statement is true or True.\n",
    "\n",
    "如果语句为 `False` 或 `false`，则返回 `true`。如果语句为 `True` 或 `true`，则返回 `false`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 155,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "True\n",
      "False\n",
      "~x\n",
      "~x\n",
      "~((A | B) & (~A | ~B))\n"
     ]
    }
   ],
   "source": [
    "from sympy import Not, And, Or\n",
    "from sympy.abc import x, A, B\n",
    "print(Not(True))\n",
    "print(Not(False))\n",
    "print(Not(And(True, False)))\n",
    "print(Not(Or(True, False)))\n",
    "print(Not(And(And(True, x), Or(x, False))))\n",
    "print(~x)\n",
    "print(Not(And(Or(A, B), Or(~A, ~B))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 注释\n",
    "\n",
    "提供 `~` 操作符是为了方便，但请注意，它在这里的使用与 Python 中的正常使用不同，Python 中的正常使用是按位的，而 `~` 不是按位的。特别是，如果 `a` 是一个整数，那么 `~a` 和 `Not(a)`将是不同的。此外，由于 Python 子类中的 `bools` 来自 `int`，因此 `~True` 与 `~1` 相同，后者是 `-2`，其布尔值为 `True`。若要避免此问题，请使用 SymPy 布尔类型 `true` 和 `false`。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 156,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "-2\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy import true\n",
    "print(~True)\n",
    "print(~true)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Xor(*args)\n",
    "\n",
    "逻辑异或(exclusive OR)函数。\n",
    "\n",
    "Returns True if an odd number of the arguments are True and the rest are False.\n",
    "\n",
    "如果参数中有奇数个 `True`，其余为 `False`，则返回 `True`。\n",
    "\n",
    "Returns False if an even number of the arguments are True and the rest are False.\n",
    "\n",
    "如果参数中有偶数个 `True`，其余为 `False`，则返回 `False`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 157,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "True\n",
      "False\n",
      "x ^ y\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Xor\n",
    "from sympy import symbols\n",
    "x, y = symbols('x y')\n",
    "print(Xor(True, False))\n",
    "print(Xor(True, True))\n",
    "print(Xor(True, False, True, True, False))\n",
    "print(Xor(True, False, True, False))\n",
    "print(x ^ y)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 注释\n",
    "\n",
    "The ^ operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise xor. In particular, a ^ b and Xor(a, b) will be different if a and b are integers.\n",
    "\n",
    "提供 `^` 操作符是为了方便，但请注意，它在这里的使用与 Python 中的正常使用不同，Python 中的正常使用是按位 `xor`。特别是，如果 `a` 和 `b` 是整数，那么 `a ^ b` 和 `Xor(a，b)`将会不同。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 158,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle x$"
      ],
      "text/plain": [
       "x"
      ]
     },
     "execution_count": 158,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Xor(x, y).subs(y, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Nand(*args)\n",
    "\n",
    "逻辑与非函数。\n",
    "\n",
    "它按顺序计算自己的参数，如果其中任何一个参数为 `False`，则立即给出 `True`，如果全部为 `True`，则给出 `False`。\n",
    "\n",
    "如果任何参数为 `False`，则返回 `True`; 如果所有参数为 `True`，则返回 `False`\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 159,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "~(x & y)\n",
      "~(x & y)\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Nand\n",
    "from sympy import symbols\n",
    "x, y = symbols('x y')\n",
    "print(Nand(False, True))\n",
    "print(Nand(True, True))\n",
    "print(Nand(x, y))\n",
    "print(~(x & y))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Nor(*args)\n",
    "\n",
    "逻辑 NOR 函数。\n",
    "\n",
    "它按顺序计算自己的参数，如果其中任何一个参数为 `True`，则立即给出 `False`，如果全部为 `False`，则给出 `True`。\n",
    "\n",
    "如果任何参数为 `True`，则返回 `False`; 如果所有参数为 `False`，则返回 `True`\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 160,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "False\n",
      "False\n",
      "True\n",
      "~(x | y)\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Nor\n",
    "from sympy import symbols\n",
    "x, y = symbols('x y')\n",
    "print(Nor(True, False))\n",
    "print(Nor(True, True))\n",
    "print(Nor(False, True))\n",
    "print(Nor(False, False))\n",
    "print(Nor(x, y))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Xnor(*args)\n",
    "\n",
    "逻辑 XNOR 函数。\n",
    "\n",
    "如果奇数个参数的为 `True`，其余为 `False`，则返回 `False`。\n",
    "\n",
    "如果参数的偶数为 `True`，其余为 `False`，则返回 `True`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 161,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "False\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Xnor\n",
    "from sympy import symbols\n",
    "x, y = symbols('x y')\n",
    "print(Xnor(True, False))\n",
    "print(Xnor(True, True))\n",
    "print(Xnor(True, False, True, True, False))\n",
    "print(Xnor(True, False, True, False))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Implies(*args)\n",
    "\n",
    "逻辑蕴涵。\n",
    "\n",
    "`A` 蕴涵 `B` 等价于如果 `A` 那么 `B`，在数学上，它被写成 `~A | B`。\n",
    "\n",
    "接受两个布尔参数; 如果 `A` 为 `True`，`B` 为 `False` 则返回 `False`，其他情况返回 `True`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 162,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "True\n",
      "True\n",
      "Implies(x, y)\n",
      "Implies(x, y)\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Implies\n",
    "from sympy import symbols\n",
    "x, y = symbols('x y')\n",
    "print(Implies(True, False))\n",
    "print(Implies(False, False))\n",
    "print(Implies(True, True))\n",
    "print(Implies(False, True))\n",
    "print(x >> y)\n",
    "print(y << x)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 注释\n",
    "\n",
    "提供 `>>` 和 `<<` 操作符是为了方便，但请注意，它们在这里的用法不同于 Python 中的常规用法，即位移。因此，如果 `a` 和 `b` 是整数，则 `Implies (a，b)`和 `a >> b` 将返回不同的结果。特别是，因为 Python 认为 `True` 和 `False` 是整数，所以 `True >> True` 将与`1 >> 1`相同，即`0`，真值为 `False`。为了避免这个问题，可以使用 SymPy 对象 `true` 和 `false`。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 163,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy import true, false\n",
    "print(True >> False)\n",
    "print(true >> false)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Equivalent(*args)\n",
    "\n",
    "等价关系。\n",
    "\n",
    "当`Equivalent(a，b)`为 `True` 当且仅当 `a` 和 `b` 都为 `True` 或都为 `False`。\n",
    "\n",
    "如果所有参数在逻辑上是等价的，则返回 `True`，否则返回 `False`。\n",
    "\n",
    "对于两个参数，这相当于 Xnor。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 164,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Equivalent, And\n",
    "from sympy.abc import x\n",
    "print(Equivalent(False, False, False))\n",
    "print(Equivalent(True, False, False))\n",
    "print(Equivalent(x, And(x, True)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.ITE(*args)\n",
    "\n",
    "`If-then-else` 子句。\n",
    "\n",
    "`ITE(A, B, C)`如果 `A` 为真，则返回 `B` 的结果，否则返回 `C` 的结果。所有参数必须是布尔值。\n",
    "\n",
    "从逻辑门的角度来看，`ITE` 对应于`2-to-1`多路复用器，其中 `A` 是选择信号。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 165,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "ITE(x, y, z)\n",
      "x\n",
      "y\n",
      "y\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import ITE, And, Xor, Or\n",
    "from sympy.abc import x, y, z\n",
    "print(ITE(True, False, True))\n",
    "print(ITE(Or(True, False), And(True, True), Xor(True, True)))\n",
    "print(ITE(x, y, z))\n",
    "print(ITE(True, x, y))\n",
    "print(ITE(False, x, y))\n",
    "print(ITE(x, y, y))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "尝试使用非布尔型参数会生成一个 TypeError:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 166,
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "expecting bool or Boolean, not `[]`.",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mTypeError\u001b[0m                                 Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-166-773a5ec7e383>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mITE\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;32mTrue\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/boolalg.py\u001b[0m in \u001b[0;36m__new__\u001b[0;34m(cls, *args, **kwargs)\u001b[0m\n\u001b[1;32m   1453\u001b[0m                     \u001b[0ma\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m~\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m   1454\u001b[0m         \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 1455\u001b[0;31m             a, b, c = BooleanFunction.binary_check_and_simplify(\n\u001b[0m\u001b[1;32m   1456\u001b[0m                 a, b, c)\n\u001b[1;32m   1457\u001b[0m         \u001b[0mrv\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/boolalg.py\u001b[0m in \u001b[0;36mbinary_check_and_simplify\u001b[0;34m(self, *args)\u001b[0m\n\u001b[1;32m    464\u001b[0m     \u001b[0;32mdef\u001b[0m \u001b[0mbinary_check_and_simplify\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m*\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    465\u001b[0m         \u001b[0;32mfrom\u001b[0m \u001b[0msympy\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcore\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mrelational\u001b[0m \u001b[0;32mimport\u001b[0m \u001b[0mRelational\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mEq\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mNe\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 466\u001b[0;31m         \u001b[0margs\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0mas_Boolean\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0margs\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    467\u001b[0m         \u001b[0mbin\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mset\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0munion\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mbinary_symbols\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0margs\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    468\u001b[0m         \u001b[0mrel\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mset\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0munion\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0matoms\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mRelational\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0margs\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/boolalg.py\u001b[0m in \u001b[0;36m<listcomp>\u001b[0;34m(.0)\u001b[0m\n\u001b[1;32m    464\u001b[0m     \u001b[0;32mdef\u001b[0m \u001b[0mbinary_check_and_simplify\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m*\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    465\u001b[0m         \u001b[0;32mfrom\u001b[0m \u001b[0msympy\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcore\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mrelational\u001b[0m \u001b[0;32mimport\u001b[0m \u001b[0mRelational\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mEq\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mNe\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 466\u001b[0;31m         \u001b[0margs\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0mas_Boolean\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0margs\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    467\u001b[0m         \u001b[0mbin\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mset\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0munion\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mbinary_symbols\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0margs\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    468\u001b[0m         \u001b[0mrel\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mset\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0munion\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mi\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0matoms\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mRelational\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mi\u001b[0m \u001b[0;32min\u001b[0m \u001b[0margs\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/boolalg.py\u001b[0m in \u001b[0;36mas_Boolean\u001b[0;34m(e)\u001b[0m\n\u001b[1;32m     58\u001b[0m     \u001b[0;32mif\u001b[0m \u001b[0misinstance\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0me\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mBoolean\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m     59\u001b[0m         \u001b[0;32mreturn\u001b[0m \u001b[0me\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 60\u001b[0;31m     \u001b[0;32mraise\u001b[0m \u001b[0mTypeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'expecting bool or Boolean, not `%s`.'\u001b[0m \u001b[0;34m%\u001b[0m \u001b[0me\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m     61\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m     62\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mTypeError\u001b[0m: expecting bool or Boolean, not `[]`."
     ]
    }
   ],
   "source": [
    "ITE(True, [], ())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 类 class sympy.logic.boolalg.Exclusive(*args)\n",
    "\n",
    "如果只有一个参数为 `True` 或没有参数为 `True`，则为 `True`。\n",
    "\n",
    "`Exclusive (a，b，c)`等价于 `~ (a & b) & ~ (a & c) & ~ (b & c)`。\n",
    "\n",
    "对于两个参数，这相当于 Xor。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from sympy.logic.boolalg import Exclusive\n",
    "print(Exclusive(False, False, False))\n",
    "print(Exclusive(False, True, False))\n",
    "print(Exclusive(False, True, True))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "下面的函数可以用来处理代数形式`Algebraic`、合取形式`Conjunctive`、析取形式`Disjunctive`和反规范形式`Negated Normal`:\n",
    "\n",
    "### 方法 sympy.logic.boolalg.to_anf(expr, deep=True)\n",
    "\n",
    "将 expr 转换为代数范式(ANF `Algebraic Normal Form`)。\n",
    "\n",
    "`ANF`是标准规范形，这意味着两个等价公式可以转换成相同的`ANF`。\n",
    "\n",
    "如果逻辑表达式具有以下形式，则它是代数范式 `ANF`\n",
    "\n",
    "$$ 1 \\oplus a \\oplus b \\oplus ab \\oplus abc $$\n",
    "\n",
    "例如，它可以是:\n",
    "- 完全真,\n",
    "- 完全假,\n",
    "- 变量的连接,\n",
    "- 逻辑异或。\n",
    "\n",
    "逻辑异或只能包含 `true`、变量或变量的连接，不允许否定。\n",
    "\n",
    "如果 `deep` 为 `False`，则布尔表达式的参数被视为变量，即只有顶层表达式被转换为 ANF。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "A ^ True\n",
      "A ^ B ^ (A & B) ^ (A & C) ^ (B & C) ^ (A & B & C)\n",
      "True ^ ~A ^ (~A & (Equivalent(B, C)))\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent\n",
    "from sympy.logic.boolalg import to_anf\n",
    "from sympy.abc import A, B, C\n",
    "print(to_anf(Not(A)))\n",
    "print(to_anf(And(Or(A, B), Not(C))))\n",
    "print(to_anf(Implies(Not(A), Equivalent(B, C)), deep=False))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.to_cnf(expr, simplify=False, force=False)\n",
    "\n",
    "将命题逻辑句子 `expr` 转换为合取范式: `((A | ~B | ...) & (B | C | ...) & ...)`。如果 `simplify` 参数为 `True`，那么 `expr` 将使用奎因－麦克拉斯基(Quine-McCluskey)算法函数计算到其最简单的 `CNF` 形式; 如果变量超过8个，并且`force`参数为 `True` (默认值为 `False`) ，那么这可能需要耗费很长计算时间。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(D | ~A) & (D | ~B)\n",
      "A | B\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import to_cnf\n",
    "from sympy.abc import A, B, D\n",
    "print(to_cnf(~(A | B) | D))\n",
    "print(to_cnf((A | B) & (A | ~A), True))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.to_dnf(expr, simplify=False, force=False)\n",
    "\n",
    "将命题逻辑句子 `expr` 转换为析取范式: `((A & ~B & ...) | (B & C & ...) | ...)`。如果参数 `simplify` 为 `True`，那么 `expr` 将使用奎因－麦克拉斯基算法(Quine-McCluskey algorithm)函数计算到其最简单的 `DNF` 形式; 如果变量超过8个，并且要求将参数`force`设置为 `True` (默认值为 `False`) ，那么这可能需要很长时间计算。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(A & B) | (B & C)\n",
      "A | C\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import to_dnf\n",
    "from sympy.abc import A, B, C\n",
    "print(to_dnf(B & (A | C)))\n",
    "print(to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.to_nnf(expr, simplify=True)\n",
    "\n",
    "将 `expr` 转换为否定范式`NNF`( Negation Normal Form)。\n",
    "\n",
    "如果逻辑表达式只包含 `And`、 `Or` 和 `Not`，而 `Not` 仅应用于标量，则该表达式是 `NNF` 否定范式。如果 `simplify` 为 `True`，则结果中不包含冗余子句。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(A | B) & (~C | ~D)\n",
      "(A | ~B | (A & ~B)) & (B | ~A | (B & ~A))\n"
     ]
    }
   ],
   "source": [
    "from sympy.abc import A, B, C, D\n",
    "from sympy.logic.boolalg import Not, Equivalent, to_nnf\n",
    "print(to_nnf(Not((~A & ~B) | (C & D))))\n",
    "print(to_nnf(Equivalent(A >> B, B >> A)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.is_anf(expr)\n",
    "\n",
    "检查 `expr` 是否为代数范式ANF(`Algebraic Normal Form`)。\n",
    "\n",
    "如果逻辑表达式具有以下形式，则它是代数范式 `ANF`\n",
    "\n",
    "例如, 它是`永真式`，`永假式`，`变量连接`, `逻辑异或`。`逻辑异或`只能包含 `true`、`变量`或`变量连接`。不允许`否定`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import And, Not, Xor, true, is_anf\n",
    "from sympy.abc import A, B, C\n",
    "print(is_anf(true))\n",
    "print(is_anf(A))\n",
    "print(is_anf(And(A, B, C)))\n",
    "print(is_anf(Xor(A, Not(B))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.is_cnf(expr)\n",
    "\n",
    "测试一个表达式是否是合取范式。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import is_cnf\n",
    "from sympy.abc import A, B, C\n",
    "print(is_cnf(A | B | C))\n",
    "print(is_cnf(A & B & C))\n",
    "print(is_cnf((A & B) | C))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.is_dnf.(expr)\n",
    "\n",
    "测试一个表达式是否是`析取范式`(disjunctive normal)。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "\n",
    "from sympy.logic.boolalg import is_dnf\n",
    "from sympy.abc import A, B, C\n",
    "print(is_dnf(A | B | C))\n",
    "print(is_dnf(A & B & C))\n",
    "print(is_dnf((A & B) | C))\n",
    "print(is_dnf(A & (B | C)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.is_nnf(expr, simplified=True)\n",
    "\n",
    "检查 `expr` 是否为否定范式NNF(`Negation Normal Form`)。\n",
    "\n",
    "如果逻辑表达式只包含 `And`、 `Or` 和 `Not`，而 `Not` 仅应用于文字，则该表达式在 `NNF` 中。如果 `simplified` 为 `True`，则检查结果是否包含冗余子句。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "True\n",
      "False\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy.abc import A, B, C\n",
    "from sympy.logic.boolalg import Not, is_nnf\n",
    "print(is_nnf(A & B | ~C))\n",
    "print(is_nnf((A | ~A) & (B | C)))\n",
    "print(is_nnf((A | ~A) & (B | C), False))\n",
    "print(is_nnf(Not(A & B) | C))\n",
    "print(is_nnf((A >> B) & (B >> A)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.gateinputcount(expr)\n",
    "\n",
    "返回实现布尔表达式的逻辑门的输入总数。\n",
    "\n",
    "#### 返回 int\n",
    "\n",
    "门输入数目\n",
    "\n",
    "#### 注意\n",
    "\n",
    "并非所有的布尔函数在这里都算作门，只有那些被认为是标准门的函数才算。这些是: `And`，`Or`，`Xor`，`Not`，和 `ITE` (多路复用器 multiplexer)。`Nand`，`Nor`和 `Xnor` 将被评估为 `Not(And())`等。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "ename": "ImportError",
     "evalue": "cannot import name 'gateinputcount' from 'sympy.logic' (/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/__init__.py)",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mImportError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-24-b3772226d21a>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfrom\u001b[0m \u001b[0msympy\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mlogic\u001b[0m \u001b[0;32mimport\u001b[0m \u001b[0mgateinputcount\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;31mImportError\u001b[0m: cannot import name 'gateinputcount' from 'sympy.logic' (/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/__init__.py)"
     ]
    }
   ],
   "source": [
    "from sympy.logic import gateinputcount"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "ename": "ImportError",
     "evalue": "cannot import name 'gateinputcount' from 'sympy.logic' (/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/__init__.py)",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mImportError\u001b[0m                               Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-1-a491ea89743d>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfrom\u001b[0m \u001b[0msympy\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mlogic\u001b[0m \u001b[0;32mimport\u001b[0m \u001b[0mAnd\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mOr\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mNand\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mNot\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mgateinputcount\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m      2\u001b[0m \u001b[0;32mfrom\u001b[0m \u001b[0msympy\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mabc\u001b[0m \u001b[0;32mimport\u001b[0m \u001b[0mx\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0my\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mz\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      3\u001b[0m \u001b[0mexpr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mAnd\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0my\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      4\u001b[0m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mgateinputcount\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m      5\u001b[0m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mgateinputcount\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mOr\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mexpr\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mz\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mImportError\u001b[0m: cannot import name 'gateinputcount' from 'sympy.logic' (/opt/anaconda3/lib/python3.8/site-packages/sympy/logic/__init__.py)"
     ]
    }
   ],
   "source": [
    "from sympy.logic import And, Or, Nand, Not, gateinputcount\n",
    "from sympy.abc import x, y, z\n",
    "expr = And(x, y)\n",
    "print(gateinputcount(expr))\n",
    "print(gateinputcount(Or(expr, z)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "注意 `Nand` 被自动计算为 `Not(And())` 所以 `gateinputcount(Nand(x, y, z))` 输出4,  `gateinputcount(Not(And(x, y, z)))` 也输出4\n",
    "\n",
    "然而可以通过使用 `evaluate = False` 使得 `gateinputcount(Nand(x, y, z, evaluate=False))` 输出3， 来避免这种情况\n",
    "\n",
    "还要注意，比较将计算为一个布尔变量: `gateinputcount(And(x > z, y >= 2))` 输出2\n",
    "\n",
    "作为一个符号: > > > `gateinputcount(x)` 输出0\n",
    "\n",
    "## Simplification and equivalence-testing 简化和等价性检验\n",
    "\n",
    "### 方法 sympy.logic.boolalg.simplify_logic(expr, form=None, deep=True, force=False)\n",
    "\n",
    "这个功能将布尔函数简化为 `SOP` 或 `POS` 形式的简化版本。返回类型是 `SymPy` 中的 `Or` 或 `And` 对象。\n",
    "\n",
    "#### 参数\n",
    "\n",
    "- expr : Boolean Expression\n",
    "\n",
    "布尔表达式\n",
    "\n",
    "- form: string (`cnf`或`dnf`)或 `None` (默认值)。\n",
    "\n",
    "如果`cnf`或`dnf`，则返回相应标准形式的最简单表达式; 如果`None`，则返回具有最少参数的表达式(默认为 `CNF`)。\n",
    "\n",
    "- deep : bool (缺省值为 True)\n",
    "\n",
    "指示是否递归简化输入中包含的任何非布尔函数。\n",
    "\n",
    "- force : bool (默认为 False)\n",
    "\n",
    "由于这些简化需要耗费变量数量为指数的时间耗费，所以在默认情况下对8个变量的表达式作为限制。当表达式的变量大于8个时，只进行符号简化(由深度控制)。通过将`force`设置为`True`，该限制将被移除。请注意，这可能会导致很长的简化时间。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "~x & ~y\n",
      "(z & ~x & ~y) | (~x & ~y & ~z)\n",
      "~x & ~y\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic import simplify_logic\n",
    "from sympy.abc import x, y, z\n",
    "from sympy import S\n",
    "b = (~x & ~y & ~z) | ( ~x & ~y & z)\n",
    "print(simplify_logic(b))\n",
    "print(S(b))\n",
    "print(simplify_logic(S(b)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "SymPy 的 `simplify()`函数还可用于将逻辑表达式简化为最简单的形式。\n",
    "\n",
    "### 方法 sympy.logic.boolalg.bool_map(bool1, bool2)\n",
    "\n",
    "返回 `bool1`的简化版本，使得 `bool1`和 `bool2`表达式的变量映射表示两个变量之间的一些对应关系的相同的逻辑行为。如果存在多个此类映射，则只返回其中一个。\n",
    "\n",
    "例如，对于映射`{ x: a，y: b }`或`{ x: b，y: a }` ，`And(x，y)`在逻辑上等价于 `And(a，b)`。如果不存在这样的映射，则返回 `False`。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(y & ~z, {y: a, z: b})\n"
     ]
    }
   ],
   "source": [
    "from sympy import SOPform, bool_map, Or, And, Not, Xor\n",
    "from sympy.abc import w, x, y, z, a, b, c, d\n",
    "function1 = SOPform([x, z, y],[[1, 0, 1], [0, 0, 1]])\n",
    "function2 = SOPform([a, b, c],[[1, 0, 1], [1, 0, 0]])\n",
    "print(bool_map(function1, function2))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "结果不一定是唯一的，但它们是规范的。这里，`(y，z)`可以是`(a，d)`或`(d，a)` :"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "((x & y) | (w & ~y) | (z & ~y), {w: a, z: d, x: b, y: c})\n",
      "(c & d & (a | b) & (~a | ~b), {c: d, d: x, a: a, b: b})\n"
     ]
    }
   ],
   "source": [
    "eq =  Or(And(Not(y), w), And(Not(y), z), And(x, y))\n",
    "eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c))\n",
    "print(bool_map(eq, eq2))\n",
    "eq = And(Xor(a, b), c, And(c,d))\n",
    "print(bool_map(eq, eq.subs(c, x)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Manipulating expressions 操作表达式\n",
    "\n",
    "下面的函数可以用来操作布尔表达式:\n",
    "\n",
    "### 方法 sympy.logic.boolalg.distribute_and_over_or(expr)\n",
    "\n",
    "给定一个变量的`合取式`和`析取式`组成的表达式 `expr`, 返回 `CNF` 的等价句。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(A \\vee \\neg B\\right) \\wedge \\left(A \\vee \\neg C\\right)$"
      ],
      "text/plain": [
       "(A | ~B) & (A | ~C)"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.logic.boolalg import distribute_and_over_or, And, Or, Not\n",
    "from sympy.abc import A, B, C\n",
    "distribute_and_over_or(Or(A, And(Not(B), Not(C))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.distribute_or_over_and(expr)\n",
    "\n",
    "给定一个变量的`合取式`和`析取式`组成的表达式 `expr`，返回 `DNF` 的等价句。\n",
    "\n",
    "注意，输出没有被化简。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(B \\wedge C\\right) \\vee \\left(C \\wedge \\neg A\\right)$"
      ],
      "text/plain": [
       "(B & C) | (C & ~A)"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.logic.boolalg import distribute_or_over_and, And, Or, Not\n",
    "from sympy.abc import A, B, C\n",
    "distribute_or_over_and(And(Or(Not(A), B), C))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.distribute_xor_over_and(expr)\n",
    "\n",
    "给定的`expr`是一个布尔量的`合取式`或`异或式`，返回一个等价的逻辑`异或式`。\n",
    "\n",
    "注意，输出没有简化。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle \\left(B \\wedge C\\right) \\veebar \\left(C \\wedge \\neg A\\right)$"
      ],
      "text/plain": [
       "(B & C) ^ (C & ~A)"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.logic.boolalg import distribute_xor_over_and, And, Xor, Not\n",
    "from sympy.abc import A, B, C\n",
    "distribute_xor_over_and(And(Xor(Not(A), B), C))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.eliminate_implications(expr)\n",
    "\n",
    "改变`逻辑蕴含式`和`等价式`为`And`, `Or` 和 `Not`。 即, 返回等效的逻辑表达式仅包含 `&`, `|` 和 `~`逻辑操作符。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "B | ~A\n",
      "(A | ~B) & (B | ~A)\n",
      "(A | ~C) & (B | ~A) & (C | ~B)\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import Implies, Equivalent,          eliminate_implications\n",
    "from sympy.abc import A, B, C\n",
    "print(eliminate_implications(Implies(A, B)))\n",
    "print(eliminate_implications(Equivalent(A, B)))\n",
    "print(eliminate_implications(Equivalent(A, B, C)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Truth tables and related functions 真值表及相关函数\n",
    "\n",
    "为布尔函数创建真值表是可行的。\n",
    "\n",
    "### 方法 sympy.logic.boolalg.truth_table(expr, variables, input=True)\n",
    "\n",
    "返回输入变量的所有可能值的生成器，以及这些可能值对该布尔表达式的计算结果。\n",
    "\n",
    "#### 参数\n",
    "\n",
    "- expr : Boolean expression\n",
    "- variables : list of variables\n",
    "- input : bool (默认 True)\n",
    "\n",
    "指示是否返回输入组合。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 0] -> True\n",
      "[0, 1] -> True\n",
      "[1, 0] -> False\n",
      "[1, 1] -> True\n",
      "[([0, 0], False), ([0, 1], True), ([1, 0], True), ([1, 1], True)]\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import truth_table\n",
    "from sympy.abc import x,y\n",
    "table = truth_table(x >> y, [x, y])\n",
    "for t in table:\n",
    "    print('{0} -> {1}'.format(*t))\n",
    "table = truth_table(x | y, [x, y])\n",
    "print(list(table))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "如果`input`为 `False`，则真值表`truth_table`只返回值为`True`的列表。在这种情况下，可以从给定输出的索引中推导出相应的变量输入值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[True, False, True, True]\n",
      "[(y, 0), (x, 0)] -> True\n",
      "[(y, 0), (x, 1)] -> False\n",
      "[(y, 1), (x, 0)] -> True\n",
      "[(y, 1), (x, 1)] -> True\n"
     ]
    }
   ],
   "source": [
    "from sympy.utilities.iterables import ibin\n",
    "vars = [y, x]\n",
    "values = truth_table(x >> y, vars, input=False)\n",
    "values = list(values)\n",
    "print(values)\n",
    "for i, value in enumerate(values):\n",
    "    print('{0} -> {1}'.format(list(zip(vars, ibin(i, len(vars)))), value))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "对于整数描述的映射的`0`和`1`及符号到真值表位置之间的映射，可以使用以下函数:\n",
    "\n",
    "### 方法 sympy.logic.boolalg.integer_to_term(n, bits=None, str=False)\n",
    "\n",
    "返回与 `n` 的二进制值对应的长度位列表，小位向右(最后一位)。如果位被省略，那么长度将是表示 n 所需的数字。如果按相反的顺序需要位，请使用返回列表的`[::-1]`片。\n",
    "\n",
    "如果需要一个从`[0,0，... ，0]`到`[1,1，... ，1]`的所有位长度列表序列，则为位传递一个非整数，例如`all`。\n",
    "\n",
    "如果所需的位字符串为 pass str = True。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[1, 0]\n",
      "[0, 0, 1, 0]\n"
     ]
    }
   ],
   "source": [
    "from sympy.utilities.iterables import ibin\n",
    "print(ibin(2))\n",
    "print(ibin(2, 4))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "如果所有列表对应于0到2 * * n-1，传递一个非整数位:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(0, 0)\n",
      "(0, 1)\n",
      "(1, 0)\n",
      "(1, 1)\n"
     ]
    }
   ],
   "source": [
    "bits = 2\n",
    "for i in ibin(2, 'all'):\n",
    "    print(i)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "如果需要一个给定长度的位字符串，使用 str = True:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0001111011\n",
      "1101111000\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "['000', '001', '010', '011', '100', '101', '110', '111']"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "n = 123\n",
    "bits = 10\n",
    "print(ibin(n, bits, str=True))\n",
    "print(ibin(n, bits, str=True)[::-1])  # small bits left\n",
    "list(ibin(3, 'all', str=True))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.term_to_integer(term)\n",
    "\n",
    "返回一个整数，该整数对应于由术语给出的以2为基数的数字。\n",
    "\n",
    "#### 参数\n",
    "\n",
    "- term : a string or list of ones and zeros\n",
    "\n",
    "一个字符串或一串0和1\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "4\n",
      "4\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import term_to_integer\n",
    "print(term_to_integer([1, 0, 0]))\n",
    "print(term_to_integer('100'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 方法 sympy.logic.boolalg.bool_maxterm(k, variables)\n",
    "\n",
    "返回第 k 个最大项。\n",
    "\n",
    "每个 `maxterm` 根据 `minterms` 使用的相反的传统二进制编码分配一个索引。`Maxterm` 约定将值`0`分配给直接形式，`1`分配给补形式。\n",
    "\n",
    "#### 参数\n",
    "\n",
    "- k : int 或`1`和`0`的列表 (互补模式)\n",
    "\n",
    "- variables : list of variables\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "y | ~x | ~z\n",
      "z | ~x | ~y\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import bool_maxterm\n",
    "from sympy.abc import x, y, z\n",
    "print(bool_maxterm([1, 0, 1], [x, y, z]))\n",
    "print(bool_maxterm(6, [x, y, z]))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 参考资料\n",
    "\n",
    "[R555] https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_maxterms\n",
    "\n",
    "### 方法 sympy.logic.boolalg.bool_minterm(k, variables)\n",
    "\n",
    "返回k次最小项\n",
    "\n",
    "最小项是由变量的互补模式的二进制编码来编号的。这个约定将值1赋给直接形式，将值0赋给补形式。\n",
    "\n",
    "#### 参数\n",
    "\n",
    "k : int 或1和0的列表 (补语式)\n",
    "\n",
    "variables : list of variables\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x & z & ~y\n",
      "x & y & ~z\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import bool_minterm\n",
    "from sympy.abc import x, y, z\n",
    "print(bool_minterm([1, 0, 1], [x, y, z]))\n",
    "print(bool_minterm(6, [x, y, z]))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 参考资料\n",
    "\n",
    "R556 https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_minterms\n",
    "\n",
    "### 方法 sympy.logic.boolalg.bool_monomial(k, variables)\n",
    "\n",
    "返回 k 次单项式。\n",
    "\n",
    "单项式用二进制编码来表示变量的存在和缺失。这个约定将值1赋给变量的存在，将值0赋给没有变量的存在。\n",
    "\n",
    "每个布尔函数都可以用一个 `Zhegalkin` 多项式(代数范式)唯一表示。布尔函数的 `Zhegalkin` 多项式可包含多达2 n 个单项式。我们可以列举所有的单项式。每个单项式完全由每个变量的存在或不存在来确定。\n",
    "\n",
    "例如，具有4个变量(a，b，c，d)的布尔函数最多可以包含24 = 16\n",
    "单项式。13次单项式是 a & b & d 的乘积，因为13在二进制中是1,1,0,1。\n",
    "\n",
    "#### 参数\n",
    "\n",
    "- k : int or list of 1’s and 0’s\n",
    "- variables : list of variables\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "x & z\n",
      "x & y\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import bool_monomial\n",
    "from sympy.abc import x, y, z\n",
    "print(bool_monomial([1, 0, 1], [x, y, z]))\n",
    "print(bool_monomial(6, [x, y, z]))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### sympy.logic.boolalg.anf_coeffs(truthvalues)\n",
    "\n",
    "将一些布尔表达式的真值列表转换为表示 ANF 中布尔表达式的多项式 mod 2(逻辑异或)的系数列表(即“ Zhegalkin 多项式”)。\n",
    "\n",
    "有可能`Zhegalkin`单项式在变量中，因为每个单项式完全由每个变量的存在或不存在指定。\n",
    "\n",
    "我们可以列举出所有的单项式。例如，具有4个变量(a，b，c，d)的布尔函数最多可以包含$2^4 = 16$个单项式。13次单项式是 `a & b & d` 的乘积，因为13在二进制中是1,1,0,1。\n",
    "\n",
    "一个给定的单项式在一个多项式中的存在或不存在对应于单项式的系数分别为1或0。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 1, 1, 0, 0, 0, 1, 0]\n",
      "b ^ c ^ (a & b)\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.boolalg import anf_coeffs, bool_monomial, Xor\n",
    "from sympy.abc import a, b, c\n",
    "truthvalues = [0, 1, 1, 0, 0, 1, 0, 1]\n",
    "coeffs = anf_coeffs(truthvalues)\n",
    "print(coeffs)\n",
    "polynomial = Xor(*[\n",
    "    bool_monomial(k, [a, b, c])\n",
    "    for k, coeff in enumerate(coeffs) if coeff == 1\n",
    "])\n",
    "print(polynomial)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### sympy.logic.boolalg.to_int_repr(clauses, symbols)\n",
    "\n",
    "接受 `CNF` 格式的子句，并将它们放入整数表示形式。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy.logic.boolalg import to_int_repr\n",
    "from sympy.abc import x, y\n",
    "to_int_repr([x | y, y], [x, y]) == [{1, 2}, {2}]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Inference 推论\n",
    "\n",
    "这个模块在命题逻辑中实现了一些推理例程。\n",
    "\n",
    "可满足的函数将测试给定的布尔表达式是否可满足，也就是说，您可以为变量赋值以使句子为真。\n",
    "\n",
    "例如，表达式 `x & ~ x` 是不可满足的，因为 `x` 没有值使这个断言成为 `True`。另一方面，`(x | y) & (x | y) & (~ x | y)`是可满足的，当`x` 和 `y` 都为 `True`时。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "{x: True, y: True}\n"
     ]
    }
   ],
   "source": [
    "from sympy.logic.inference import satisfiable\n",
    "from sympy import Symbol\n",
    "x = Symbol('x')\n",
    "y = Symbol('y')\n",
    "print(satisfiable(x & ~x))\n",
    "print(satisfiable((x | y) & (x | ~y) & (~x | y)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "正如你所看到的，当一个句子是可满足的，它返回一个使这个句子成为 True 的模型。如果不能得到满足，它就会返回错误。\n",
    "\n",
    "### 方法 sympy.logic.inference.satisfiable(expr, algorithm=None, all_models=False, minimal=False)\n",
    "\n",
    "检查命题句的可满足性。成功时返回一个模型。对于普通的真表达式返回{ true: true }。\n",
    "\n",
    "在将 `all_models` 设置为 `True` 时，如果给定 `expr` 是可满足的，则返回一个模型生成器。但是，如果 `expr` 不可满足，则返回包含单个元素 `False` 的生成器。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{A: True, B: False}\n",
      "False\n",
      "{True: True}\n",
      "False\n",
      "{A: False, B: True}\n",
      "{A: True, B: True}\n",
      "{A: False}\n",
      "None\n",
      "UNSAT\n"
     ]
    }
   ],
   "source": [
    "from sympy.abc import A, B\n",
    "from sympy.logic.inference import satisfiable\n",
    "print(satisfiable(A & ~B))\n",
    "print(satisfiable(A & ~A))\n",
    "print(satisfiable(True))\n",
    "print(next(satisfiable(A & ~A, all_models=True)))\n",
    "models = satisfiable((A >> B) & B, all_models=True)\n",
    "print(next(models))\n",
    "print(next(models))\n",
    "def use_models(models):\n",
    "    for model in models:\n",
    "        if model:\n",
    "            # Do something with the model.\n",
    "            print(model)\n",
    "        else:\n",
    "            # Given expr is unsatisfiable.\n",
    "            print(\"UNSAT\")\n",
    "print(use_models(satisfiable(A >> ~A, all_models=True)))\n",
    "use_models(satisfiable(A ^ A, all_models=True))"
   ]
  }
 ],
 "metadata": {
  "interpreter": {
   "hash": "e7370f93d1d0cde622a1f8e1c04877d8463912d04d973331ad4851f04de6915a"
  },
  "kernelspec": {
   "display_name": "Python 3.9.5 64-bit",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.8"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
